equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
A weak equivalence is a morphism in a category which is supposed to be a true equivalence in a higher categorical refinement of .
The bare minimum of axioms to be satisfied by a weak equivalence are encoded in the concepts of category with weak equivalences and homotopical category. For such categories one can consider
the corresponding homotopy category, which is the universal solution to turning all weak equivalences into isomorphisms;
the corresponding -category, which is, roughly, the universal solution to turning all weak equivalences into higher categorical equivalences. There are various versions of this construction depending on what model for -categories is chosen.
The Dwyer-Kan localization uses simplicially enriched categories to model -categories.
If we use complete Segal spaces or quasicategories to model -categories, then the construction is a version of fibrant replacement.
Often, categories having weak equivalences also have extra structure that makes them easier to work with. A very powerful, and commonly occurring, level of such structure is called a model structure. There are also various weaker levels of structure, such as a category of fibrant objects.
A weak homotopy equivalence is a weak equivalence in the classical model structure on topological spaces.
A simplicial weak equivalence is a weak equivalence in the classical model structure on simplicial sets.
An equivariant weak homotopy equivalence is a weak equivalence in the fine model structure on topological G-spaces.
A weak equivalence in the folk model structure on Cat is a functor that is fully faithful and essentially surjective.
In homotopy type theory, a functor between internal categories in HoTT and is called a “weak equivalence” if it is fully faithful and essentially surjective.
For univalent categories there is no difference between weak equivalences and equivalences.
Last revised on June 7, 2022 at 15:55:16. See the history of this page for a list of all contributions to it.